es:ES, a, b:E. (b < a)  (es-height(es;b) < es-height(es;a)) 

latex

Definitions	WellFnd{i}(A;x,y.R(x;y)), x. t(x), {T}, x.A(x), E, P  Q, (e < e'), , Type, a < b, es-height(es;e), x:A. B(x), x:AB(x), {x:A| B(x)} , , t  T, ES, left + right, Unit, P  Q, P & Q, x:A  B(x), A, b, s = t, , sender(e), False, A c B, P  Q, e < e', if b then t else f fi , t.1, let x,y = A in B(x;y), SQType(T), s ~ t, A  B, P  Q, T, True, pred(e), i <z j, i z j, b, n+m, #$n
Lemmas	es-pred wf, es-sender wf, bnot wf, le wf, le int wf, bool wf, lt int wf, es-pred-causl, assert of le int, bnot of lt int, assert wf, assert of lt int, es-sender-causl, es-causl-iff, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, nat wf, es-height wf, es-causl wf, es-E wf, es-causl-wellfnd